module fn.logic.fol.syntax.Parser

open System




open FParsec.Primitives
open FParsec.CharParsers
open FParsec.OperatorPrecedenceParser

open fn.adt.Tree
open fn.adt.tree.build.Parser
open fn.adt.tree.search.Pattern
open fn.text.Patterns
open fn.logic.fol.syntax.Formula
open fn.logic.fol.syntax.Scheme


(* bug workaround *)
let manyChars p = many p |>> List.toArray |>> (fun x -> new String(x))


type FolFormulaParser () =
    let token x =
        let success, res = Int32.TryParse x
        let v = if success then res :> obj 
                else 
                    let success, res = Double.TryParse x
                    if success then res :> obj else x :> obj
        Identifier.make v

    let symbol = manyChars (choice [| letter; digit; anyOf ".|?_" |]) |>> token
    let lsymbol = between (pchar '[') (pchar ']') (manyChars (noneOf "]")) |>> token
    let opp = OperatorPrecedenceParser<_,_>()
    let expr = opp.ExpressionParser
    let tree = TreeParser(lsymbol <|> symbol, (fun x -> expr))
    let ws = spaces
    let mk2 root lhs rhs = Node(Identifier.make root, [lhs; rhs])
    let mk1 root arg = Node(Identifier.make root, [arg])
    do
      opp.TermParser <- tree.Tree
      for KeyValue(o, precedence) in FolFormula.INFIXES do
        opp.AddOperator(InfixOp(o, ws, precedence, Assoc.Left, mk2 o))
      for KeyValue(o, precedence) in FolFormula.PREFIXES do
        opp.AddOperator(PrefixOp(o, ws, precedence, true, mk1 o))

    member this.Expression = expr
    member this.parse (input : string) = 
        match run (ws >>. expr .>> eof) input with
        | Success(a,_,_) -> this.post(FolFormula a)
        | Failure(msg,_,_) -> failwith msg
    member this.post (formula : FolFormula) =
        formula |@ FolFormula.INTRINSICS


module SyntaxSugar =
    let formula = FolFormulaParser ()

    let to_wild_f (i : Identifier) =
        match i.literal.ToString() with
        | Prefix "?" marker -> Any { i with literal=marker }
        | _ -> Literal i
    
    let to_pattern_f (t: FolFormula) = FolFormula<_> (t.e.apply_to_values to_wild_f)
    
    let ( !! ) (t: string) = FolScheme (to_pattern_f (formula.parse t))
    let ( ! ) (t: string) = (formula.parse t)

